es:ES, e', e:E, i:.
(i < ||[e, e']||)
 (firstn(i;[e, e']) = if (i = 0) then [] else [e, pred([e, e'][i])] fi   (E List)) 

latex

Definitions

t  T, x:A. B(x), E, ||as||, b, P  Q, False, A, A  B, , [e, e'], l[i], pred(e), firstn(n;as), , b, , (i = j), P & Q, P  Q, Unit, if b then t else f fi , (e <loc e'), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), ES, t.1, x,y. t(x;y), P  Q, P  Q, e loc e' , i  j < k, {i..j}, Top, S  T, SQType(T), Trans(T;x,y.E(x;y)), True, T, hd(l), i <z j, i z j, as @ bs, Dec(P), first(e), i  j , t  ...$L

Lemmas

firstn length, select append back, length nil, length cons, non neg length, select append front, nat properties, es-first wf, firstn append, length-append, bool cases, bool sq, es-pred-locl, decidable lt, es-interval-less, es-le-trans3, hd-es-interval, squash wf, true wf, es-le-trans, first0, top wf, l before select, le wf, l before-es-interval, and functionality wrt iff, wellfounded functionality wrt iff, es-locl-iff, event system wf, es-locl-wellfnd, es-locl wf, nat wf, length wf1, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, firstn wf, es-pred wf, select wf, es-interval wf, es-E wf